<html>
<body>
Contains classes immediately related to the translation of bytecode classes to
BoogiePL.

<p>
The main entry point to the translation is the
{@link b2bpl.translation.Translator Translator} class which accepts a set of
bytecode classes and translates them to a single BoogiePL program. The actual
translation process is thereby split over different classes to which the
{@code Translator} delegates part of the translation. In particular, the
following classes actively contribute to the resulting BoogiePL program during
the translation process:
<ul>
  <li>
    The already introduced {@link b2bpl.translation.Translator Translator} class
    is responsible for generating the global theory of the BoogiePL program.
    This mainly includes the static part of the background predicate such as
    the axiomatizations of the heap and the JVM's type system but also the
    dynamic global declarations which are generated in response to special
    references (type/field/literal... references) encountered during every
    individual translation session.
  </li>
  <li>
    The {@link b2bpl.translation.MethodTranslator MethodTranslator} class is
    responsible for translating a bytecode method to a single procedure in
    BoogiePL. The translation of a method not only includes the translation of
    the individual bytecode instructions but also the generation of proof
    obligations and assumptions as required or justified, respectively, by the
    verification methodology used.
  </li>
  <li>
    The {@link b2bpl.translation.SpecificationTranslator SpecificationTranslator}
    class is used to translate BML specification expressions to BoogiePL.
    Specialized factory methods are provided for creating instances of the class
    suitable for translating specification expressions appearing in different
    contexts, such as inside an invariant declaration or inside a method's
    postcondition.
  </li>
  <li>
    The {@link b2bpl.translation.ModifiesFilter ModifiesFilter} class is used to
    translate BML store references appearing inside the modifies clause of a
    method or a loop specification.
  </li>
</ul>
Since some special references such as field or type references appearing in
bytecode instructions or BML specifications cannot be resolved locally but
instead require a set of global declarations to be created in the BoogiePL
program, the special interface {@link b2bpl.translation.TranslationContext
TranslationContext} is defined which should always be used to translate those
references. The main purpose of having such a separate interface is to decouple
the individual classes contributing to the translation process from each other.
In the current implementation, the {@code TranslationContext} interface is
internally implemented by the {@code Translator} while every other translator
class accepts such an interface which is then used to trigger the translation
of the encountered references.
</p>
</body>
</html>
